T:Type, L:(T List), P:({x:T| (x  L)} ).
(xL. Dec(P(x)))  (L':T List. (L'  L & (x:T. (x  L')  ((x  L) & P(x))))) 

latex

ProofTree

Definitions

Type, , t  T, type List, A List, s = t, x:AB(x), x:A. B(x), [car / cdr], (x  l), {x:A| B(x)} , f(a), x(s), Dec(P), x.A(x), x. t(x), xL. P(x), L1  L2, x:A  B(x), P & Q, P  Q, x:A. B(x), P  Q, P  Q, [], suptype(S; T), #$n, {i..j}, i  j < k, A c B, S  T, |g|, l[i], , , A  B, A, False, Void, ||as||, a < b, increasing(f;k), P  Q, left + right, True, b, b | a, a ~ b, a  b, a <p b, a < b, x f y, (xL.P(x)), Atom, , x,y:A//B(x;y), |p|, |r|, last(L), {T}, <a, b>, s ~ t, SQType(T), filter(P;l), hd(l), i <z j, i z j, n+m, i  j

Lemmas

select member, non neg length, cons sublist cons, implies functionality wrt iff, all functionality wrt iff, false wf, guard wf, not wf, cons member, nil sublist, select wf, length wf2, nat wf, subtype rel wf, member wf, rev implies wf, le wf, int seg wf, length wf1, increasing wf, nil member, iff wf, sublist wf, l all wf, decidable wf, l member wf